es:ES, x, i:Id, T:Type, c:T.
(x, y:T. Dec(x = y  T))
 vartype(i;x)  T
 (e:E. loc(e) = i  first(e)  (x when e) = c)
 (e':E.
 (loc(e') = i  (x after e') = c  (ev:E. ev  e'  & (x after ev) = (x when ev)  T)) 

latex

Definitions	A & B, x when e, x:A. B(x), E, P  Q, Id, loc(e), t  T, (x after e), ES, Dec(P), x:A. B(x), P & Q, e  e' , A, b, first(e), Prop, vartype(i;x)
Lemmas	es-when wf, es-first wf, assert wf, es-loc wf, es-after wf, not wf, es-vartype wf, es-E wf, decidable wf, Id wf, event system wf, es-first-exists, es-le-loc, change-lemma, es-le wf